The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
    ↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳6 CdtProblem
    ↳7 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳12 CdtProblem
↳13 CpxTrsMatchBoundsTAProof (⇔, 10 ms)
↳14 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

p(p(b(a(x0)), x1), p(x2, x3)) → p(p(x3, a(x2)), p(b(a(x1)), b(x0)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(z3, a(z2)), p(b(a(z1)), b(z0)))
Tuples:

P(p(b(a(z0)), z1), p(z2, z3)) → c(P(p(z3, a(z2)), p(b(a(z1)), b(z0))), P(z3, a(z2)), P(b(a(z1)), b(z0)))
S tuples:

P(p(b(a(z0)), z1), p(z2, z3)) → c(P(p(z3, a(z2)), p(b(a(z1)), b(z0))), P(z3, a(z2)), P(b(a(z1)), b(z0)))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace P(p(b(a(z0)), z1), p(z2, z3)) → c(P(p(z3, a(z2)), p(b(a(z1)), b(z0))), P(z3, a(z2)), P(b(a(z1)), b(z0))) by

P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(x3, a(x2)), p(b(a(x1)), b(x0))))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(z3, a(z2)), p(b(a(z1)), b(z0)))
Tuples:

P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(x3, a(x2)), p(b(a(x1)), b(x0))))
S tuples:

P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(x3, a(x2)), p(b(a(x1)), b(x0))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(5) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace P(p(b(a(x0)), x1), p(x2, x3)) → c(P(p(x3, a(x2)), p(b(a(x1)), b(x0)))) by

P(p(b(a(z0)), a(x2)), p(b(a(x1)), b(x0))) → c(P(p(b(x0), a(b(a(x1)))), p(b(a(a(x2))), b(z0))))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(z3, a(z2)), p(b(a(z1)), b(z0)))
Tuples:

P(p(b(a(z0)), a(x2)), p(b(a(x1)), b(x0))) → c(P(p(b(x0), a(b(a(x1)))), p(b(a(a(x2))), b(z0))))
S tuples:

P(p(b(a(z0)), a(x2)), p(b(a(x1)), b(x0))) → c(P(p(b(x0), a(b(a(x1)))), p(b(a(a(x2))), b(z0))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(7) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace P(p(b(a(z0)), a(x2)), p(b(a(x1)), b(x0))) → c(P(p(b(x0), a(b(a(x1)))), p(b(a(a(x2))), b(z0)))) by

P(p(b(a(z0)), a(b(a(x2)))), p(b(a(a(x1))), b(x0))) → c(P(p(b(x0), a(b(a(a(x1))))), p(b(a(a(b(a(x2))))), b(z0))))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(z3, a(z2)), p(b(a(z1)), b(z0)))
Tuples:

P(p(b(a(z0)), a(b(a(x2)))), p(b(a(a(x1))), b(x0))) → c(P(p(b(x0), a(b(a(a(x1))))), p(b(a(a(b(a(x2))))), b(z0))))
S tuples:

P(p(b(a(z0)), a(b(a(x2)))), p(b(a(a(x1))), b(x0))) → c(P(p(b(x0), a(b(a(a(x1))))), p(b(a(a(b(a(x2))))), b(z0))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(p(b(a(z0)), a(b(a(x2)))), p(b(a(a(x1))), b(x0))) → c(P(p(b(x0), a(b(a(a(x1))))), p(b(a(a(b(a(x2))))), b(z0)))) by

P(p(b(a(z0)), a(b(a(z1)))), p(b(a(a(z2))), b(a(y0)))) → c(P(p(b(a(y0)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(z0))))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(z3, a(z2)), p(b(a(z1)), b(z0)))
Tuples:

P(p(b(a(z0)), a(b(a(z1)))), p(b(a(a(z2))), b(a(y0)))) → c(P(p(b(a(y0)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(z0))))
S tuples:

P(p(b(a(z0)), a(b(a(z1)))), p(b(a(a(z2))), b(a(y0)))) → c(P(p(b(a(y0)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(z0))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace P(p(b(a(z0)), a(b(a(z1)))), p(b(a(a(z2))), b(a(y0)))) → c(P(p(b(a(y0)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(z0)))) by

P(p(b(a(a(y3))), a(b(a(z1)))), p(b(a(a(z2))), b(a(z3)))) → c(P(p(b(a(z3)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(a(y3)))))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

p(p(b(a(z0)), z1), p(z2, z3)) → p(p(z3, a(z2)), p(b(a(z1)), b(z0)))
Tuples:

P(p(b(a(a(y3))), a(b(a(z1)))), p(b(a(a(z2))), b(a(z3)))) → c(P(p(b(a(z3)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(a(y3)))))
S tuples:

P(p(b(a(a(y3))), a(b(a(z1)))), p(b(a(a(z2))), b(a(z3)))) → c(P(p(b(a(z3)), a(b(a(a(z2))))), p(b(a(a(b(a(z1))))), b(a(y3)))))
K tuples:none
Defined Rule Symbols:

p

Defined Pair Symbols:

P

Compound Symbols:

c

(13) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 0.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
b0(0) → 0
a0(0) → 0
p0(0, 0) → 1

(14) BOUNDS(O(1), O(n^1))